(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const _3-0 (_ BitVec 3))
(declare-const v6 Bool)
(declare-const _16-0 (_ BitVec 16))
(declare-const v8 Bool)
(declare-const v10 Bool)
(assert (or (bvsgt (bvlshr _3-0 _3-0) _3-0)))
(assert (or (= _16-0 _16-0)))
(assert (or v10 (=> v5 (or (not (bvsgt (bvlshr _3-0 _3-0) _3-0)) (not (bvsgt (bvlshr _3-0 _3-0) _3-0)) (= _3-0 _3-0 _3-0) v4 v2)) v0 (=> v5 (or (not (bvsgt (bvlshr _3-0 _3-0) _3-0)) (not (bvsgt (bvlshr _3-0 _3-0) _3-0)) (= _3-0 _3-0 _3-0) v4 v2)) v0 v10))
(assert (or v8 v10))
(assert (or v8 v8 v0 v0 v6))
(assert (or (=> v5 (or (not (bvsgt (bvlshr _3-0 _3-0) _3-0)) (not (bvsgt (bvlshr _3-0 _3-0) _3-0)) (= _3-0 _3-0 _3-0) v4 v2)) (bvsgt (bvlshr _3-0 _3-0) _3-0) v0))
(check-sat)
